(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_LRA)
(declare-fun v0 () Real)
(assert (let ((e1 2))
(let ((e2 (+ v0 v0)))
(let ((e3 (+ e2 v0)))
(let ((e4 (+ e3 v0)))
(let ((e5 (- v0)))
(let ((e6 (/ e1 e1)))
(let ((e7 (distinct v0 e2)))
(let ((e8 (> e2 e4)))
(let ((e9 (= e4 e4)))
(let ((e10 (>= e3 e5)))
(let ((e11 (distinct v0 e6)))
(let ((e12 (ite e9 e4 e5)))
(let ((e13 (ite e10 e12 e4)))
(let ((e14 (ite e7 e3 e4)))
(let ((e15 (ite e8 e6 e14)))
(let ((e16 (ite e8 e6 e2)))
(let ((e17 (ite e7 v0 e12)))
(let ((e18 (ite e11 e3 e16)))
(let ((e19 (< e16 e15)))
(let ((e20 (distinct e16 v0)))
(let ((e21 (> e16 e12)))
(let ((e22 (distinct e6 e5)))
(let ((e23 (< e14 v0)))
(let ((e24 (distinct e15 e17)))
(let ((e25 (> e12 e17)))
(let ((e26 (>= e2 e6)))
(let ((e27 (<= v0 v0)))
(let ((e28 (<= e13 e17)))
(let ((e29 (= e17 e3)))
(let ((e30 (< e4 e3)))
(let ((e31 (< e2 e5)))
(let ((e32 (> v0 e17)))
(let ((e33 (<= e14 e2)))
(let ((e34 (>= e18 e4)))
(let ((e35 (not e30)))
(let ((e36 (xor e21 e29)))
(let ((e37 (=> e27 e10)))
(let ((e38 (= e22 e25)))
(let ((e39 (=> e24 e8)))
(let ((e40 (and e23 e32)))
(let ((e41 (or e40 e38)))
(let ((e42 (ite e34 e9 e33)))
(let ((e43 (not e11)))
(let ((e44 (=> e7 e7)))
(let ((e45 (or e19 e28)))
(let ((e46 (xor e39 e37)))
(let ((e47 (xor e36 e41)))
(let ((e48 (ite e35 e35 e47)))
(let ((e49 (not e46)))
(let ((e50 (or e20 e48)))
(let ((e51 (not e26)))
(let ((e52 (= e43 e44)))
(let ((e53 (xor e52 e50)))
(let ((e54 (or e31 e53)))
(let ((e55 (ite e51 e45 e51)))
(let ((e56 (not e54)))
(let ((e57 (=> e49 e42)))
(let ((e58 (=> e57 e55)))
(let ((e59 (and e58 e56)))
e59
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
